package verifier;

import dk.brics.automaton.State;
import model.DeltaForwardingGraph;
import model.LabeledEdge;
import network.Device;
import util.Logger;
import util.StopWatch;

import java.util.HashMap;
import java.util.HashSet;

public class DPVerifier {
    private DeltaForwardingGraph dfg;
    private HashSet<Property> properties;
    private HashMap<String, HashSet<Integer>> dp;

    public DPVerifier(DeltaForwardingGraph dfg, HashSet<Property> properties) {
        this.dfg = dfg;
        this.properties = properties;
    }

    public void checkInvariants() {
        int size = dfg.graph.vertexSet().size(), i, j, k;
        Object[][] A = new Object[size][size];

        for (i = 0; i < size; i++)  {
            for(j = 0; j < size; j++) {
                A[i][j] = new HashSet<>();
            }
        }

        i = 0;
        HashMap<Device, Integer> deviceToId = new HashMap<>();
        HashMap<Integer, Device> idToDevice = new HashMap<>();
        for (Device device : dfg.graph.vertexSet()) {
            if (device.getName().contentEquals("default")) continue;
            deviceToId.put(device, i);
            idToDevice.put(i, device);
            i ++;
        }

        for (Device s : dfg.graph.vertexSet()) {
            if (s.getName().contentEquals("default")) continue;
            i = deviceToId.get(s);
            for (LabeledEdge edge : dfg.graph.edgesOf(s))
                if (edge.getFrom() == s) {
                    if (edge.getTo().getName() == "default") {
                        // Logger.addVerificationReports("DP-based Verifier", "Blackhole", s.getName());
                        return;
                    }
                    j = deviceToId.get(edge.getTo());
                    ((HashSet<Integer>) A[i][j]).addAll(edge.getPredicates());
                }
        }

        StopWatch.StopWatch();
        for (k = 0; k < size; k++) {
            for (i = 0; i < size; i++)  {
                for(j = 0; j < size; j++) {
                    HashSet<Integer> t = new HashSet<>(((HashSet<Integer>) A[i][k]));
                    t.retainAll(((HashSet<Integer>) A[k][j]));
                    ((HashSet<Integer>) A[i][j]).addAll(t);
                }
            }
        }

        for (i = 0; i < size; i ++)
            if (!((HashSet<Integer>) A[i][i]).isEmpty()){
                // Logger.addVerificationReports("DP-based Verifier ", "Loop", idToDevice.get(i).getName());
            }
    }

    public void checkPolicy() {
        this.dp = new HashMap<>();

        for (Property property: this.properties) {
            if (!this.dfg.graph.vertexSet().contains(property.getSource())) { // delta not affect source
                continue;
            }
            HashSet<Integer> pset = (HashSet<Integer>) this.dfg.transferredPreds.clone();
            HashSet<Device> history = new HashSet<>();
            this.traverseReach(property.getSource(), pset, history, property.getAutomata().getInitialState());
        }
    }

    private void traverseReach(Device s, HashSet<Integer> pset, HashSet<Device> history, State currentState) {
        String key = s.getName() + currentState.toString();
        HashSet<Integer> ext = dp.get(key);
        if (ext != null) {
            pset.retainAll(ext);
            if (pset.isEmpty()) {
                return;
            }
            ext.addAll(pset);
        } else {
            dp.put(key, (HashSet<Integer>) pset.clone());
        }

        if (history.contains(s)) {
            // Logger.addVerificationReports("DP-based Verifier" , "Loop", s.getName());
            return;
        }

        for (LabeledEdge edge : this.dfg.graph.edgesOf(s)) {
            if (edge.getFrom() == s) {
                if (edge.getTo().getName() == "default") {
                    return;
                }
                HashSet<Integer> npset = (HashSet<Integer>) pset.clone();
                npset.retainAll(edge.getPredicates());
                State nextState = currentState;
                for (char c : s.getName().toCharArray()) {
                    nextState = nextState.step(c);
                }
                if (nextState == null) return;
                HashSet<Device> nhistory = (HashSet<Device>) history.clone();
                nhistory.add(s);
                this.traverseReach(edge.getTo(), npset, nhistory, nextState);
            }
        }
    }
}